/*
 * Clause.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include "bfr/Clause.hpp"

#include <string>
#include <iostream>
#include <sstream>

#include "bfr/Literal.hpp"

namespace bfr {

Clause::Clause()
    : literals(), maxID(0) { }

Clause::Clause(size_t initialSize)
    : literals(2 * initialSize), maxID(0) { }

Clause::~Clause() { }

bool Clause::add(const Literal &literal) {
    const size_t id = literal.getId();
    if (id > maxID) {
        maxID = id;
    }
    return literals.insert(literal).second;
}

std::string Clause::asString() const {
    std::ostringstream stream;
    stream << *this;
    return stream.str();
}

size_t Clause::hashValue() const {
    size_t result = 0;

    const_iterator e = end();

    for(const_iterator it = begin();
            it != e;
            it++) {
        result += (*it).hashValue();
    }
    return result;
}

bool Clause::operator ==(const Clause &other) const {
   if (size() != other.size()) {
       return false;
   }
   const_iterator e = end();
   const_iterator it = begin();
   while (it != e) {
       if (!other.contains(*it)) {
           return false;
       }
       it++;
   }
   return true;
}

bool Clause::contains(const Literal &literal) const {
    return literals.count(literal);
}

size_t Clause::size() const {
    return literals.size();
}

Clause::const_iterator Clause::begin() const {
    return literals.begin();
}

Clause::const_iterator Clause::end() const {
    return literals.end();
}

size_t Clause::getMaxLiteralId() const {
    return maxID;
}

} // namespace bfr
